Termination proof of /tmp/tmpQK7wH3/A13.itrs

Termination of the given ITRSProblem could successfully be proven:

↳ ITRS

  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

divNat(TRUE, x, y) → d(x, y, 0@z)
cond(FALSE, x, y, z) → 0@z
dNat(TRUE, x, y, z) → cond(>=@z(x, z), x, -@z(y, 1@z), z)
cond(TRUE, x, y, z) → +@z(1@z, d(x, +@z(y, 1@z), +@z(+@z(y, 1@z), z)))
d(x, y, z) → dNat(&&(&&(>=@z(x, 0@z), >=@z(y, 1@z)), >=@z(z, 0@z)), x, y, z)
div(x, y) → divNat(&&(>=@z(x, 0@z), >=@z(y, 1@z)), x, y)

The set Q consists of the following terms:

divNat(TRUE, x0, x1)
cond(FALSE, x0, x1, x2)
dNat(TRUE, x0, x1, x2)
cond(TRUE, x0, x1, x2)
d(x0, x1, x2)
div(x0, x1)

Added dependency pairs

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

divNat(TRUE, x, y) → d(x, y, 0@z)
cond(FALSE, x, y, z) → 0@z
dNat(TRUE, x, y, z) → cond(>=@z(x, z), x, -@z(y, 1@z), z)
cond(TRUE, x, y, z) → +@z(1@z, d(x, +@z(y, 1@z), +@z(+@z(y, 1@z), z)))
d(x, y, z) → dNat(&&(&&(>=@z(x, 0@z), >=@z(y, 1@z)), >=@z(z, 0@z)), x, y, z)
div(x, y) → divNat(&&(>=@z(x, 0@z), >=@z(y, 1@z)), x, y)

The integer pair graph contains the following rules and edges:

(0): DIV(x[0], y[0]) → DIVNAT(&&(>=@z(x[0], 0@z), >=@z(y[0], 1@z)), x[0], y[0])
(1): DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])
(2): DIVNAT(TRUE, x[2], y[2]) → D(x[2], y[2], 0@z)
(3): D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])
(4): COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))

(0) -> (2), if ((x[0] →^* x[2])∧(y[0] →^* y[2])∧(&&(>=@z(x[0], 0@z), >=@z(y[0], 1@z)) →^* TRUE))

(1) -> (4), if ((z[1] →^* z[4])∧(x[1] →^* x[4])∧(-@z(y[1], 1@z) →^* y[4])∧(>=@z(x[1], z[1]) →^* TRUE))

(2) -> (3), if ((y[2] →^* y[3])∧(x[2] →^* x[3]))

(3) -> (1), if ((z[3] →^* z[1])∧(x[3] →^* x[1])∧(y[3] →^* y[1])∧(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)) →^* TRUE))

(4) -> (3), if ((+@z(y[4], 1@z) →^* y[3])∧(+@z(+@z(y[4], 1@z), z[4]) →^* z[3])∧(x[4] →^* x[3]))

The set Q consists of the following terms:

divNat(TRUE, x0, x1)
cond(FALSE, x0, x1, x2)
dNat(TRUE, x0, x1, x2)
cond(TRUE, x0, x1, x2)
d(x0, x1, x2)
div(x0, x1)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(0): DIV(x[0], y[0]) → DIVNAT(&&(>=@z(x[0], 0@z), >=@z(y[0], 1@z)), x[0], y[0])
(1): DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])
(2): DIVNAT(TRUE, x[2], y[2]) → D(x[2], y[2], 0@z)
(3): D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])
(4): COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))

(0) -> (2), if ((x[0] →^* x[2])∧(y[0] →^* y[2])∧(&&(>=@z(x[0], 0@z), >=@z(y[0], 1@z)) →^* TRUE))

(1) -> (4), if ((z[1] →^* z[4])∧(x[1] →^* x[4])∧(-@z(y[1], 1@z) →^* y[4])∧(>=@z(x[1], z[1]) →^* TRUE))

(2) -> (3), if ((y[2] →^* y[3])∧(x[2] →^* x[3]))

(3) -> (1), if ((z[3] →^* z[1])∧(x[3] →^* x[1])∧(y[3] →^* y[1])∧(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)) →^* TRUE))

(4) -> (3), if ((+@z(y[4], 1@z) →^* y[3])∧(+@z(+@z(y[4], 1@z), z[4]) →^* z[3])∧(x[4] →^* x[3]))

The set Q consists of the following terms:

divNat(TRUE, x0, x1)
cond(FALSE, x0, x1, x2)
dNat(TRUE, x0, x1, x2)
cond(TRUE, x0, x1, x2)
d(x0, x1, x2)
div(x0, x1)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(4): COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))
(1): DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])
(3): D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])

(1) -> (4), if ((z[1] →^* z[4])∧(x[1] →^* x[4])∧(-@z(y[1], 1@z) →^* y[4])∧(>=@z(x[1], z[1]) →^* TRUE))

(3) -> (1), if ((z[3] →^* z[1])∧(x[3] →^* x[1])∧(y[3] →^* y[1])∧(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)) →^* TRUE))

(4) -> (3), if ((+@z(y[4], 1@z) →^* y[3])∧(+@z(+@z(y[4], 1@z), z[4]) →^* z[3])∧(x[4] →^* x[3]))

The set Q consists of the following terms:

divNat(TRUE, x0, x1)
cond(FALSE, x0, x1, x2)
dNat(TRUE, x0, x1, x2)
cond(TRUE, x0, x1, x2)
d(x0, x1, x2)
div(x0, x1)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4])) the following chains were created:

We consider the chain DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1]), COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4])), D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
(1)    (>=@z(x[1], z[1])=TRUE∧x[1]=x[4]∧z[1]=z[4]∧+@z(y[4], 1@z)=y[3]∧x[4]=x[3]∧+@z(+@z(y[4], 1@z), z[4])=z[3]∧-@z(y[1], 1@z)=y[4] ⇒ COND(TRUE, x[4], y[4], z[4])≥NonInfC∧COND(TRUE, x[4], y[4], z[4])≥D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))

We simplified constraint (1) using rules (III), (IV) which results in the following new constraint:
(2)    (>=@z(x[1], z[1])=TRUE ⇒ COND(TRUE, x[1], -@z(y[1], 1@z), z[1])≥NonInfC∧COND(TRUE, x[1], -@z(y[1], 1@z), z[1])≥D(x[1], +@z(-@z(y[1], 1@z), 1@z), +@z(+@z(-@z(y[1], 1@z), 1@z), z[1]))∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x[1] + (-1)z[1] ≥ 0 ⇒ (U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥)∧1 + (-1)Bound + (-1)z[1] + x[1] ≥ 0∧0 ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x[1] + (-1)z[1] ≥ 0 ⇒ (U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥)∧1 + (-1)Bound + (-1)z[1] + x[1] ≥ 0∧0 ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x[1] + (-1)z[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + (-1)z[1] + x[1] ≥ 0∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x[1] + (-1)z[1] ≥ 0 ⇒ 0 = 0∧0 = 0∧1 + (-1)Bound + (-1)z[1] + x[1] ≥ 0∧0 ≥ 0∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x[1] ≥ 0 ⇒ 0 = 0∧0 = 0∧1 + (-1)Bound + x[1] ≥ 0∧0 ≥ 0∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))

We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(8)    (x[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 = 0∧0 = 0∧1 + (-1)Bound + x[1] ≥ 0∧0 ≥ 0∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))

(9)    (x[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 = 0∧0 = 0∧1 + (-1)Bound + x[1] ≥ 0∧0 ≥ 0∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))

For Pair DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1]) the following chains were created:

We consider the chain D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3]), DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1]), COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4])) which results in the following constraint:
(10)    (&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z))=TRUE∧>=@z(x[1], z[1])=TRUE∧x[3]=x[1]∧y[3]=y[1]∧x[1]=x[4]∧z[1]=z[4]∧z[3]=z[1]∧-@z(y[1], 1@z)=y[4] ⇒ DNAT(TRUE, x[1], y[1], z[1])≥NonInfC∧DNAT(TRUE, x[1], y[1], z[1])≥COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])∧(U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥))

We simplified constraint (10) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(11)    (>=@z(x[3], z[3])=TRUE∧>=@z(z[3], 0@z)=TRUE∧>=@z(x[3], 0@z)=TRUE∧>=@z(y[3], 1@z)=TRUE ⇒ DNAT(TRUE, x[3], y[3], z[3])≥NonInfC∧DNAT(TRUE, x[3], y[3], z[3])≥COND(>=@z(x[3], z[3]), x[3], -@z(y[3], 1@z), z[3])∧(U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥))

We simplified constraint (11) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(12)    (x[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥)∧0 ≥ 0∧-1 + y[3] ≥ 0)

We simplified constraint (12) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(13)    (x[3] + (-1)z[3] ≥ 0∧z[3] ≥ 0∧x[3] ≥ 0∧-1 + y[3] ≥ 0 ⇒ (U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥)∧0 ≥ 0∧-1 + y[3] ≥ 0)

We simplified constraint (13) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(14)    (z[3] ≥ 0∧-1 + y[3] ≥ 0∧x[3] ≥ 0∧x[3] + (-1)z[3] ≥ 0 ⇒ 0 ≥ 0∧-1 + y[3] ≥ 0∧(U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥))

We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(15)    (z[3] ≥ 0∧-1 + y[3] ≥ 0∧z[3] + x[3] ≥ 0∧x[3] ≥ 0 ⇒ 0 ≥ 0∧-1 + y[3] ≥ 0∧(U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥))

We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(16)    (z[3] ≥ 0∧y[3] ≥ 0∧z[3] + x[3] ≥ 0∧x[3] ≥ 0 ⇒ 0 ≥ 0∧y[3] ≥ 0∧(U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥))

For Pair D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3]) the following chains were created:

We consider the chain D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3]) which results in the following constraint:
(17)    (D(x[3], y[3], z[3])≥NonInfC∧D(x[3], y[3], z[3])≥DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])∧(U^Increasing(DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])), ≥))

We simplified constraint (17) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(18)    ((U^Increasing(DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

We simplified constraint (18) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(19)    ((U^Increasing(DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 ≥ 0∧0 ≥ 0)

We simplified constraint (19) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(20)    (0 ≥ 0∧0 ≥ 0∧(U^Increasing(DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])), ≥))

We simplified constraint (20) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(21)    (0 = 0∧(U^Increasing(DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))
- (x[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 = 0∧0 = 0∧1 + (-1)Bound + x[1] ≥ 0∧0 ≥ 0∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))
- (x[1] ≥ 0∧z[1] ≥ 0 ⇒ 0 = 0∧0 = 0∧1 + (-1)Bound + x[1] ≥ 0∧0 ≥ 0∧(U^Increasing(D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))), ≥))
DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])
- (z[3] ≥ 0∧y[3] ≥ 0∧z[3] + x[3] ≥ 0∧x[3] ≥ 0 ⇒ 0 ≥ 0∧y[3] ≥ 0∧(U^Increasing(COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])), ≥))
D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])
- (0 = 0∧(U^Increasing(DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])), ≥)∧0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(-@z(x₁, x₂)) = x₁ + (-1)x₂
POL(DNAT(x₁, x₂, x₃, x₄)) = -1 + (-1)x₄ + x₃ + x₂ + (-1)x₁
POL(COND(x₁, x₂, x₃, x₄)) = 1 + (-1)x₄ + x₂
POL(>=@z(x₁, x₂)) = 0
POL(0@z) = 0
POL(TRUE) = -1
POL(&&(x₁, x₂)) = -1
POL(+@z(x₁, x₂)) = x₁ + x₂
POL(D(x₁, x₂, x₃)) = (-1)x₃ + x₂ + x₁
POL(FALSE) = 1
POL(1@z) = 1
POL(undefined) = -1

The following pairs are in P_>:

COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))

The following pairs are in P_bound:

COND(TRUE, x[4], y[4], z[4]) → D(x[4], +@z(y[4], 1@z), +@z(+@z(y[4], 1@z), z[4]))

The following pairs are in P_≥:

DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])
D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])

At least the following rules have been oriented under context sensitive arithmetic replacement:

FALSE¹ → &&(FALSE, FALSE)¹
-@z¹ ↔
&&(TRUE, TRUE)¹ ↔ TRUE¹
+@z¹ ↔
FALSE¹ → &&(FALSE, TRUE)¹
FALSE¹ → &&(TRUE, FALSE)¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPNonInfProof

                ↳ IDP

                  ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(1): DNAT(TRUE, x[1], y[1], z[1]) → COND(>=@z(x[1], z[1]), x[1], -@z(y[1], 1@z), z[1])
(3): D(x[3], y[3], z[3]) → DNAT(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)), x[3], y[3], z[3])

(3) -> (1), if ((z[3] →^* z[1])∧(x[3] →^* x[1])∧(y[3] →^* y[1])∧(&&(&&(>=@z(x[3], 0@z), >=@z(y[3], 1@z)), >=@z(z[3], 0@z)) →^* TRUE))

The set Q consists of the following terms:

divNat(TRUE, x0, x1)
cond(FALSE, x0, x1, x2)
dNat(TRUE, x0, x1, x2)
cond(TRUE, x0, x1, x2)
d(x0, x1, x2)
div(x0, x1)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.